perm filename EQUIV.TEX[S79,JMC] blob
sn#456674 filedate 1979-07-07 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00006 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 \input begin.tex[tex,clt]
C00003 00003 \ctrline{\bf A SIMPLE SET THEORY PROOF IN FOL}
C00005 00004 \folalign{
C00014 00005 \folalign{
C00022 00006 I note that I haven't proved that $v$ is unique. This is easy, and
C00023 ENDMK
C⊗;
\input begin.tex[tex,clt]
\folfntdef % for FOL conversations
\output{\outmemo}
\def\pagenum{T} %print pagenumbers at bottom
\def\tpage{F} %not the title page
\setcount\pctr 1
\def\subali#1{\vbox{\halign{\hskip 20pt \lft{##}\quad⊗\lft{##}⊗\quad\lft{##}\cr #1}}}
\input fol.tex[tex,clt]
\ninefont
\ninepoint
\ctrline{\bf A SIMPLE SET THEORY PROOF IN FOL}
\ctrline{\bf John McCarthy}
Stimulated by Don Knuth's remark that proving the existence of the
set of equivalence classes of an equivalence relation was several hundred
steps in AUTOMATH, I decided to see what it came to in FOL.
We prove that the set of equivalence classes exists, that the union
of the classes is the original set, that the elements of each class
are mutually equivalent and that if two classes intersect they are
equal.
The FOL proof of the existence and some properties of the set
equivalence classes modulo an equivalence relation came to 102
steps. If it were done over, about 10 steps would be removed with
some improvement in clarity. We begin with a set of axioms for Zermelo-Fraenkel
set theory. They have been used in other proofs and only a few
of them are used in this proof.
The axioms begin with declarations of symbols. Formal declaration
statements are a feature FOL shares with programming languages. There are
two axiom schemata - replacement and separation - and both are used in
the proof.
Then we have the axioms for an equivalence relation $R(x,y)$. Further
comments are included with the proof itself.
\folalign{
\comment 0|Axioms for Zermelo-Fraenkel Set Theory\quad(AJT June 75, modified JMC).|
\*⊗DECLARE\0 INDCONST\0 nl int;\cr
\*⊗DECLARE\0 PREDCONST\0 ε 2[INF];\cr
\*⊗DECLARE\0 PREDCONST\0 ⊂ 2[INF];\cr
\*⊗DECLARE\0 OPCONST\0 ∪ 2[INF];\cr
\*⊗DECLARE\0 OPCONST\0 ∩ 2[INF];\cr
\*⊗DECLARE\0 OPCONST\0 union 1[pre];\cr
\*⊗DECLARE\0 OPCONST\0 intersect 1[pre];\cr
\*⊗DECLARE\0 INDVAR\0 r s t u v w x y z;\cr
\*⊗DECLARE\0 PREDPAR\0 A 2 B 1;\cr
\*⊗AXIOM ZF:\cr
\penalty 1000
⊗\subali{
EXT: ⊗∀x y.(∀z.(zεx≡zεy)≡x=y); ⊗\% Extensionality \cr
EMT: ⊗∀y.¬yεnl; ⊗\% Null set \cr
PAIR: ⊗∀x y w.(wε\{x,y\}≡w=x∨w=y); ⊗\% Unordered pair \cr
UNION: ⊗∀x z.(zεunion(x)≡∃t.(tεx∧zεt)); ⊗\% Sum set \cr
INTERSECT: ⊗∀x z.(zεintersect(x)≡∀t.(tεx⊃zεt)); ⊗\% Product set \cr
INF: ⊗(0εint∧∀y.(yεint⊃(y∪\{y\})εint)); ⊗\% Infinity \cr
INDUCT: ⊗B(0)∧∀x.(xεint∧B(x)⊃B(x∪\{x\}))⊃∀x.(xεint⊃B(x)); ⊗\% Induction\cr
REPL: ⊗∀x.∃y.∀z.(A(x,z)≡y=z) ⊃ ⊗\% Replacement\cr
⊗∀u.∃v.(∀r.(rεv ≡ ∃s.(sεu∧A(s,r))));\cr
SEP: ⊗∀x.∃y.∀z.(zεy≡zεx∧B(z)); ⊗\% Separation\cr
POWER: ⊗∀x.∃y.∀z.(zεy≡z⊂x); ⊗\% Power set \cr
REG: ⊗∀x.∃y.(x=0∨(yεx∧∀z.(zεx⊃¬zεy))); ⊗\% Regularity \cr
}\cr
}
\penalty 0
\folalign{
\*⊗DECLARE\0 PREDCONST\0 FUN 1,INTO 2,PSUBSET 2[INF];\cr
\*⊗DECLARE\0 OPCONST\0 rng 1 dom 1;\cr
\*⊗AXIOM SETDEFS:\cr
⊗\subalign{
SUBSET: ⊗∀x y.(x⊂y≡∀z.(zεx⊃zεy));\cr
PROPSUBSET: ⊗∀x y.(PSUBSET(x,y)≡x⊂y∧¬x=y);\cr
PAIRFUN: ⊗∀x y z.(zε\{x,y\}≡z=x∨z=y);\cr
UNITSETFUN: ⊗∀x.( \{x\}=\{x,x\} );\cr
OPAIRFUN: ⊗∀x y.( <x,y>=\{{x},{x,y}\} );\cr
FUNCTION: ⊗∀w.(FUN(w)≡∀z.(zεw⊃∃x y.(z=<x,y>))∧\cr
⊗\0 ∀x y z.(<x,y>εw∧<x,z>εw⊃y=z) );\cr
DOMAIN: ⊗∀w x.(xεdom(w)≡FUN(w)∧∃y z.(yεw∧y=<x,z>));\cr
RANGE: ⊗∀w x.(xεrng(w)≡FUN(w)∧∃y z.(yεw∧y=<z,x>));\cr
INTO: ⊗∀w x.(INTO(w,x)≡rng(w)⊂x);\cr
SUM: ⊗∀x y z.(zεx∪y≡zεx∨zεy);\cr
PRODUCT: ⊗∀x y z.(zεx∩y≡zεx∧zεy); \cr
}\cr
\comment 0|Axioms about an equivalence relation $R(x,y)$|
\*⊗DECLARE\0 PREDPAR\0 R 2;\cr
\*⊗AXIOM EQUIV:\cr
⊗\subalign{
⊗∀x.R(x,x)\cr
⊗∀x y.(R(x,y) ≡ R(y,x))\cr
⊗∀x y z.(R(x,y) ∧ R(y,z) ⊃ R(x,z))\cr
}\cr
\*⊗DECLARE\0 INDVAR\0 a;\cr
\*⊗DECLARE\0 INDVAR\0 r1 r2;\cr
}
The proof begins with a use of the axiom schema of replacement aimed
at defining the set of equivalence classes as the image of the set $a$ under
the mapping that takes each element of $a$ into its equivalence class. The
schema gives rise to an implication the premiss of which is that the
relation defines a mapping. In order to prove this, we must establish
the existence of a unique equivalence class as a set. This is begun by
the second step which uses the separation schema to define the equivalence
class of an element. Step 19 is the premiss of step 1. Its proof
does not use the fact that $R(x,y)$ is an equivalence relation. More comments
after step 21.
\folalign{
\*⊗∧I\0 REPL[A←λx t.(∀y.(yεt ≡ yεa ∧ R(x,y)))];\cr
1⊗∀x.∃y.∀z.(∀y.(yεz≡(yεa∧R(x,y)))≡y=z)⊃\cr
⊗\1 ∀u.∃v.∀r.(rεv≡∃s.(sεu∧∀y.(yεr≡(yεa∧R(s,y))))) \cr
\*⊗∧I\0 SEP[B←λy.R(x,y)];\cr
2⊗∀x1.∃y.∀z.(zεy≡(zεx1∧R(x,z))) \cr
\*⊗∀E\0 \↑\ a;\cr
3⊗∃y.∀z.(zεy≡(zεa∧R(x,z))) \cr
\*⊗∃E\0 \↑\ w;\cr
4⊗∀z.(zεw≡(zεa∧R(x,z))) (4)\cr
\*⊗ASSUME\0 ∀z.(zεt≡(zεa∧R(x,z)));\cr
5⊗∀z.(zεt≡(zεa∧R(x,z))) (5)\cr
\*⊗∀E\0 EXT w,t;\cr
6⊗∀z.(zεw≡zεt)≡w=t \cr
\*⊗∀E\0 \↑\↑\↑\ z;\cr
7⊗zεw≡(zεa∧R(x,z)) (4)\cr
\*⊗∀E\0 \↑\↑\↑\ z;\cr
8⊗zεt≡(zεa∧R(x,z)) (5)\cr
\*⊗TAUT\0 zεw≡zεt 7:8;\cr
9⊗zεw≡zεt (4 5)\cr
\*⊗∀I\0 \↑\ z;\cr
10⊗∀z.(zεw≡zεt) (4 5)\cr
\*⊗TAUT\0 w=t 6,10;\cr
11⊗w=t (4 5)\cr
\*⊗⊃I\0 5⊃\↑;\cr
12⊗∀z.(zεt≡(zεa∧R(x,z)))⊃w=t (4)\cr
\*⊗ASSUME\0 w=t;\cr
13⊗w=t (13)\cr
\*⊗SUBST\0 \↑\ IN 4;\cr
14⊗∀z.(zεt≡(zεa∧R(x,z))) (4 13)\cr
\*⊗⊃I\0 \↑\↑⊃\↑;\cr
15⊗w=t⊃∀z.(zεt≡(zεa∧R(x,z))) (4)\cr
\*⊗TAUT\0 ∀z.(zεt≡(zεa∧R(x,z)))≡w=t 12,15;\cr
16⊗∀z.(zεt≡(zεa∧R(x,z)))≡w=t (4)\cr
\*⊗∀I\0 \↑\ t;\cr
17⊗∀t.(∀z.(zεt≡(zεa∧R(x,z)))≡w=t) (4)\cr
\*⊗∃I\0 \↑\ w←y;\cr
18⊗∃y.∀t.(∀z.(zεt≡(zεa∧R(x,z)))≡y=t) \cr
\*⊗∀I\0 \↑\ x;\cr
19⊗∀x.∃y.∀t.(∀z.(zεt≡(zεa∧R(x,z)))≡y=t) \cr
\*⊗TAUT\0 ∀u.∃v.∀r.(rεv≡∃s.(sεu∧∀y.(yεr≡(yεa∧R(s,y))))) 1,19;\cr
20⊗∀u.∃v.∀r.(rεv≡∃s.(sεu∧∀y.(yεr≡(yεa∧R(s,y))))) \cr
\*⊗∀E\0 \↑\ a;\cr
21⊗∃v.∀r.(rεv≡∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y))))) \cr
}
We now have the required set of equivalence classes, and the rest of
proof is concerned with establishing its properties. By step 53 we
have established that the union of the set $v$ of equivalence classes
is the set $a$. It uses only the reflexivity of $R(x,y)$. Step 68
asserts that all the elements of an equivalence class are equivalent,
and its proof uses the symmetry and transitivity of $R(x,y)$. Step 99
asserts that if two equivalence classes intersect they are equal, and
the remaining three steps package these results into a single statement.
Neither FOL's sort mechanism nor any of its methods of simplification
are used in the proof. and it doesn't seem that they would help much.
It seems possible that Juan Bulnes's goal oriented FOL would allow
a considerably shorter proof.
\folalign{
\*⊗∃E\0 \↑\ v;\cr
22⊗∀r.(rεv≡∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y))))) (22)\cr
\*⊗∀E\0 UNION v;\cr
23⊗∀z.(zεunion v≡∃t.(tεv∧zεt)) \cr
\*⊗∀E\0 \↑\ z;\cr
24⊗zεunion v≡∃t.(tεv∧zεt) \cr
\*⊗ASSUME\0 zεunion v;\cr
25⊗zεunion v (25)\cr
\*⊗TAUT\0 ∃t.(tεv∧zεt) 24:25;\cr
26⊗∃t.(tεv∧zεt) (25)\cr
\*⊗∃E\0 \↑\ t;\cr
27⊗tεv∧zεt (27)\cr
\*⊗∀E\0 22 t;\cr
28⊗tεv≡∃s.(sεa∧∀y.(yεt≡(yεa∧R(s,y)))) (22)\cr
\*⊗TAUT\0 ∃s.(sεa∧∀y.(yεt≡(yεa∧R(s,y)))) 27:28;\cr
29⊗∃s.(sεa∧∀y.(yεt≡(yεa∧R(s,y)))) (22 27)\cr
\*⊗∃E\0 \↑\ s;\cr
30⊗sεa∧∀y.(yεt≡(yεa∧R(s,y))) (30)\cr
\*⊗∧E\0 \↑ 2;\cr
31⊗∀y.(yεt≡(yεa∧R(s,y))) (30)\cr
\*⊗∀E\0 \↑\ z;\cr
32⊗zεt≡(zεa∧R(s,z)) (30)\cr
\*⊗TAUT\0 zεa 27,32;\cr
33⊗zεa (22 25)\cr
\*⊗⊃I\0 25⊃\↑;\cr
34⊗zεunion v⊃zεa (22)\cr
\*⊗ASSUME\0 zεa;\cr
35⊗zεa (35)\cr
\*⊗∧I\0 SEP[B←λy.R(z,y)];\cr
36⊗∀x.∃y.∀z1.(z1εy≡(z1εx∧R(z,z1))) \cr
\*⊗∀E\0 \↑\ a;\cr
37⊗∃y.∀z1.(z1εy≡(z1εa∧R(z,z1))) \cr
\*⊗∃E\0 \↑\ y;\cr
38⊗∀z1.(z1εy≡(z1εa∧R(z,z1))) (38)\cr
\*⊗∧I\0 ((35 38));\cr
39⊗zεa∧∀z1.(z1εy≡(z1εa∧R(z,z1))) (35 38)\cr
\*⊗∃I\0 \↑\ z←s;\cr
40⊗∃s.(sεa∧∀z1.(z1εy≡(z1εa∧R(s,z1)))) (35 38)\cr
\*⊗∀E\0 22 y;\cr
41⊗yεv≡∃s.(sεa∧∀y1.(y1εy≡(y1εa∧R(s,y1)))) (22)\cr
\*⊗TAUT\0 yεv 40:41;\cr
42⊗yεv (22 35 38)\cr
\*⊗∀E\0 38 z;\cr
43⊗zεy≡(zεa∧R(z,z)) (38)\cr
\*⊗∀E\0 EQUIV1 z;\cr
44⊗R(z,z) \cr
\*⊗TAUT\0 zεy 35,43:44;\cr
45⊗zεy (35 38)\cr
\*⊗∧I\0 ((42 45));\cr
46⊗yεv∧zεy (22 35 38)\cr
\*⊗∃I\0 \↑\ y←t;\cr
47⊗∃t.(tεv∧zεt) (22 35)\cr
\*⊗TAUT\0 zεunion v 24,47;\cr
48⊗zεunion v (22 35)\cr
\*⊗⊃I\0 35⊃\↑;\cr
49⊗zεa⊃zεunion v (22)\cr
\*⊗TAUT\0 zεunion v≡zεa 34,49;\cr
50⊗zεunion v≡zεa (22)\cr
\*⊗∀I\0 \↑\ z;\cr
51⊗∀z.(zεunion v≡zεa) (22)\cr
\*⊗∀E\0 EXT union v,a;\cr
52⊗∀z.(zεunion v≡zεa)≡union v=a \cr
\*⊗TAUT\0 union v=a 51:52;\cr
53⊗union v=a (22)\cr
\*⊗ASSUME\0 rεv;\cr
54⊗rεv (54)\cr
\*⊗∀E\0 22 r;\cr
55⊗rεv≡∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y)))) (22)\cr
\*⊗TAUT\0 ∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y)))) 54:55;\cr
56⊗∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y)))) (22 54)\cr
\*⊗ASSUME\0 xεr∧yεr;\cr
57⊗xεr∧yεr (57)\cr
\*⊗∃E\0 \↑\↑\ s;\cr
58⊗sεa∧∀y.(yεr≡(yεa∧R(s,y))) (58)\cr
\*⊗∧E\0 \↑ 2;\cr
59⊗∀y.(yεr≡(yεa∧R(s,y))) (58)\cr
\*⊗∀E\0 \↑\ x;\cr
60⊗xεr≡(xεa∧R(s,x)) (58)\cr
\*⊗∀E\0 \↑\↑\ y;\cr
61⊗yεr≡(yεa∧R(s,y)) (58)\cr
\*⊗∀E\0 EQUIV2 s,x;\cr
62⊗R(s,x)≡R(x,s) \cr
\*⊗∀E\0 EQUIV3 x,s,y;\cr
63⊗(R(x,s)∧R(s,y))⊃R(x,y) \cr
\*⊗TAUT\0 R(x,y) 57,60:63;\cr
64⊗R(x,y) (22 54 57)\cr
\*⊗⊃I\0 57⊃\↑;\cr
65⊗(xεr∧yεr)⊃R(x,y) (22 54)\cr
\*⊗∀I\0 \↑\ x y;\cr
66⊗∀x y.((xεr∧yεr)⊃R(x,y)) (22 54)\cr
\*⊗⊃I\0 54⊃\↑;\cr
67⊗rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)) (22)\cr
\*⊗∀I\0 \↑\ r;\cr
68⊗∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y))) (22)\cr
\*⊗ASSUME\0 r1εv∧r2εv;\cr
69⊗r1εv∧r2εv (69)\cr
\*⊗ASSUME\0 ∃x.(xεr1∧xεr2);\cr
70⊗∃x.(xεr1∧xεr2) (70)\cr
\*⊗∀E\0 22 r1;\cr
71⊗r1εv≡∃s.(sεa∧∀y.(yεr1≡(yεa∧R(s,y)))) (22)\cr
\*⊗∀E\0 22 r2;\cr
72⊗r2εv≡∃s.(sεa∧∀y.(yεr2≡(yεa∧R(s,y)))) (22)\cr
\*⊗TAUT\0 ∃s.(sεa∧∀y.(yεr1≡(yεa∧R(s,y)))) 69,71;\cr
73⊗∃s.(sεa∧∀y.(yεr1≡(yεa∧R(s,y)))) (22 69)\cr
\*⊗TAUT\0 ∃s.(sεa∧∀y.(yεr2≡(yεa∧R(s,y)))) 69,72;\cr
74⊗∃s.(sεa∧∀y.(yεr2≡(yεa∧R(s,y)))) (22 69)\cr
\*⊗∃E\0 \↑\↑\ s;\cr
75⊗sεa∧∀y.(yεr1≡(yεa∧R(s,y))) (75)\cr
\*⊗∃E\0 \↑\↑\ t;\cr
76⊗tεa∧∀y.(yεr2≡(yεa∧R(t,y))) (76)\cr
\*⊗∧E\0 \↑\↑ 2;\cr
77⊗∀y.(yεr1≡(yεa∧R(s,y))) (75)\cr
\*⊗∧E\0 \↑\↑ 2;\cr
78⊗∀y.(yεr2≡(yεa∧R(t,y))) (76)\cr
\*⊗∀E\0 \↑\↑\ x;\cr
79⊗xεr1≡(xεa∧R(s,x)) (75)\cr
\*⊗∀E\0 \↑\↑\ x;\cr
80⊗xεr2≡(xεa∧R(t,x)) (76)\cr
\*⊗∀E\0 77 w;\cr
81⊗wεr1≡(wεa∧R(s,w)) (75)\cr
\*⊗∀E\0 78 w;\cr
82⊗wεr2≡(wεa∧R(t,w)) (76)\cr
\*⊗∃E\0 70 x;\cr
A: 83⊗xεr1∧xεr2 (83)\cr
\*⊗∀E\0 EQUIV2 s,w;\cr
84⊗R(s,w)≡R(w,s) \cr
\*⊗∀E\0 EQUIV2 x,t;\cr
85⊗R(x,t)≡R(t,x) \cr
\*⊗∀E\0 EQUIV2 w,t;\cr
86⊗R(w,t)≡R(t,w) \cr
\*⊗∀E\0 EQUIV2 x,s;\cr
87⊗R(x,s)≡R(s,x) \cr
\*⊗∀E\0 EQUIV3 w,s,x;\cr
88⊗(R(w,s)∧R(s,x))⊃R(w,x) \cr
\*⊗∀E\0 EQUIV3 w,x,t;\cr
89⊗(R(w,x)∧R(x,t))⊃R(w,t) \cr
\*⊗∀E\0 EQUIV3 w,t,x;\cr
90⊗(R(w,t)∧R(t,x))⊃R(w,x) \cr
\*⊗∀E\0 EQUIV3 w,x,s;\cr
B: 91⊗(R(w,x)∧R(x,s))⊃R(w,s) \cr
\*⊗TAUT\0 wεr1≡wεr2 79:B;\cr
92⊗wεr1≡wεr2 (22 69 70)\cr
\*⊗∀I\0 \↑\ w;\cr
93⊗∀w.(wεr1≡wεr2) (22 69 70)\cr
\*⊗∀E\0 EXT r1,r2;\cr
94⊗∀z.(zεr1≡zεr2)≡r1=r2 \cr
\*⊗TAUT\0 r1=r2 93:94;\cr
95⊗r1=r2 (22 69 70)\cr
\*⊗⊃I\0 70⊃\↑;\cr
96⊗∃x.(xεr1∧xεr2)⊃r1=r2 (22 69)\cr
\*⊗⊃I\0 69⊃\↑;\cr
97⊗(r1εv∧r2εv)⊃(∃x.(xεr1∧xεr2)⊃r1=r2) (22)\cr
\*⊗TAUT\0 ((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2 97;\cr
98⊗((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2 (22)\cr
\*⊗∀I\0 \↑\ r1 r2;\cr
99⊗∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2) (22)\cr
\*⊗TAUT\0 union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧\cr
⊗\1 ∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2)) 53,68,99;\cr
100⊗union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧\cr
⊗\1 ∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2)) (22)\cr
\*⊗∃I\0 \↑\ v ;\cr
101⊗∃v.(union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧\cr
⊗\1 ∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2))) \cr
\*⊗∀I\0 \↑\ a;\cr
102⊗∀a.∃v.(union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧\cr
⊗\1 ∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2))) \cr
}
I note that I haven't proved that $v$ is unique. This is easy, and
it would be an automatic byproduct of a version of the replacement schema
stating the true fact that the image set is unique. Thus uniqueness doesn't
depend on the properties of $R(x,y)$.